|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Advanced Static Analysis of Atomicity in Concurrent Programs through Facebook Infer
Harmim, Dominik ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The author of this master's thesis proposed and implemented the first version of Atomer as a plugin of the Facebook Infer framework in his bachelor's thesis. In the master's thesis, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.
|
|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
host ::
RSS.